The severity-4 "OK" diagnostic of a command or tactic previously spanned
the whole command or tactic, so the success underline covered symbol
bodies, rule right-hand sides and whole proofs. Instead:

- A command's hint is shown on its terminating ";". The command's
  recorded position stops one character before it (the parser's
  extend_pos), so lp_doc derives the ";" position from it (at_semicolon).

- Symbol declarations always create proof data, so their "OK" went
  through the proof path and landed on the symbol name. The initial
  goals stay anchored at the symbol (for the goals panel), but the
  visible hint now goes on the ";".

- A tactic's hint is shown on its leading keyword (Syntax.tactic_keyword,
  exposed as Pure.Tactic.keyword), since a tactic's end is ill-defined
  once it has subproofs. These diagnostics also anchor the goals panel,
  whose lookup (closest_before) only reads the start of each position,
  which does not move.

Also rename the lp_doc node field "ast" to "cmd".

Set the character offsets of hint positions consistently with their
columns (at_keyword left end_offset at the end of the whole tactic,
at_semicolon did not update offsets at all).

Handle a ";" at the beginning of a line: the parser's extend_pos does
not back up at column 0, so a command position with end_col = 0 cannot
distinguish a ";" at column 0 from one at column 1 (the hint used to
underline column 1, one character past a line-initial ";"). Cover both
columns in that case.

Show the "OK" hint of a command on its keyword ("symbol", "rule",
"require", ...) rather than on the terminating ";".

The keyword of a symbol, inductive or open command is not always at
the command's start (modifiers or parameters may precede it), so the
parser records the keyword position in the AST for these three
constructors. For the other commands, Syntax.command_keyword_pos
computes it as a prefix of the command's position. Tactics use the
same mechanism (tactic_keyword_pos); at_keyword and at_semicolon
disappear from lp_doc, replaced by Pos.prefix.

Additions to the pure/parsing API for the LSP server:
- Syntax.fold_paths and Pure.path_rangemap map the source ranges of
  require/open module paths; Lp_doc stores this path range map
  alongside the identifier range map
- Pure.Command.get_elt exposes the parser-level command shape so
  clients can pattern-match on declaration forms (outlines)
- Pure.set_print_state installs a document's signature state in the
  printer for correctly qualified output

- apply the workspace's lambdapi.pkg before the first document opens,
  from rootUri (pre-3.6 clients) and workspaceFolders, deduplicated —
  clients typically send both for the same directory; a package-config
  failure is logged, never fatal (the client would kill the server and
  retry in a loop)
- record snippetSupport, hierarchicalDocumentSymbolSupport and the
  completion documentationFormat, for the handlers that gate on them

- when the client supports it, answer documentSymbol with a
  DocumentSymbol[] tree built from the parsed AST: symbol declarations,
  and inductive types with their constructors as children; the flat
  SymbolInformation[] list remains the fallback
- drop the kind classification: no LSP SymbolKind matches lambdapi's
  notions (axiom, constructor, definable symbol, theorem, ...), so
  every symbol reports the least surprising kind, Function

- the module paths of require/open commands jump to the start of that
  module's file (via the path range map added with the groundwork)
- when the identifier map has no resolvable entry at the cursor, look
  up the raw token under the cursor (code-point aware) in the in-scope
  symbol table: definition keeps working in mid-edit text and in code
  past a parse error

- documentation for tactic keywords (inside proofs) and for command
  and query keywords and modifiers, sourced from doc/*.rst; the tables
  carry (name, detail, doc, snippet) so completion can reuse them
- types of the hypotheses introduced by assume, from the goal
  snapshots; names in a tactic's arguments resolve in the state before
  the tactic runs (snapshots are post-tactic, so a tactic that closes
  its subgoal or the proof used to lose its own arguments' hypotheses)
- types print with the document's own printer state (set_print_state),
  not whichever document's notations were installed last
- fallback to the token under the cursor when the identifier map
  misses: keyword docs, hypotheses and in-scope symbols hover in
  mid-edit text and past parse errors; the proof context of a broken
  edit comes from the nodes of the last parse-error-free check
  (good_nodes)

- expected-token recordings accumulate until the next consumed token
  instead of overwriting one another, and a finished application
  records that a term can be continued (a further argument, an arrow):
  syntax errors now list more of the true alternatives, with the full
  set of term starters rendered as one word: a term
- new entry point Parser.Lp.expected_tokens (exposed as
  Pure.expected_tokens): parse a source prefix and return the tokens
  the grammar accepts at its end — the command starters between
  commands, the follow set of the truncated command within one, [] on
  a syntax error before the end.  This is the follow set LSP
  completion is built on

- in-scope symbols (ghost symbols excluded; no completion kind — the
  LSP kinds don't match lambdapi's notions), offered only where the
  grammar accepts an identifier reference, never in binder positions;
  per-item type details attach lazily on completionItem/resolve
- keyword membership comes from the parser's follow sets: exactly the
  keywords the grammar accepts at the cursor are offered, with docs
  and snippets from the hover tables; when the prefix does not parse
  (a broken edit earlier in the file), fall back to the context-blind
  tables — tactics and proof enders inside proofs, command keywords
  outside, queries in both
- "." as trigger character: module paths after require/open (as a
  textEdit — "." is not a word character), qualified names after M.
  (the non-private symbols of that module, resolving require-as
  aliases; new Pure.get_aliases), flag names inside flag "..."
- hypotheses of the focused goal complete inside proofs, ranked first
  in the argument of apply, rewrite, etc.; already-typed modifiers are
  filtered from the offers

- Python tests speaking JSON-RPC over stdio to a lambdapi lsp
  subprocess: lifecycle, diagnostics, document symbols, hover,
  definition, completion (including the grammar follow-set contexts),
  goals, incremental changes, and cross-cutting invariants (range
  validity, repeated-request stability, boundary positions, both
  protocol modes)
- the tactic and query completion lists are checked against the names
  documented in doc/*.rst, so the tables cannot silently fall behind
- Python >= 3.8, standard library only; stdlib-dependent tests skip
  when no lambdapi stdlib is installed; runs as part of make test